翻訳と辞書 Words near each other ・ Dripping Springs, Delaware County, Oklahoma ・ Dripping Springs, Texas ・ Dripsey ・ Dripsey Castle Bridge ・ Dripsey Castle, Carrignamuck ・ Dripsey GAA ・ Dripsey railway station ・ Dripstick ・ Dripstone ・ Driptech ・ Driptorch ・ Drique London ・ Drinker (disambiguation) ・ Drinker Biddle & Reath ・ Drinker House ・ Drinker paradox ・ Drinker's Court ・ Drinkers Mass ・ DrinkExchange ・ Drinkin' and Courtin' ・ Drinkin' and Dreamin' ・ Drinkin' Bone ・ Drinkin' Man ・ Drinkin' Me Lonely ・ Drinkin' My Baby (Off My Mind) ・ Drinkin' My Baby Goodbye ・ Drinkin' Songs and Other Logic ・ Drinkin' Thing ・ Drinkin' Town with a Football Problem ・ Drinkin', Lechin' & Lyin' Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Drinker paradox ： ウィキペディア英語版 Drinker paradox The drinker paradox (also known as the drinker's theorem, the drinker's principle, or the drinking principle) is a theorem of classical predicate logic and not an actual paradox. Its apparently paradoxical nature comes from the way it's usually stated in natural language: ''There is someone in the pub such that, if he is drinking, then everyone in the pub is drinking''. It seems counterintuitive that 1) there is a person who is ''causing'' the others to drink, or 2) there is a person such that all through the night that one person is always the ''last'' to drink. The first objection comes from confusing formal IF…THEN statements with causation (see correlation does not imply causation). The formal statement of the theorem is timeless, eliminating the second objection because the person the statement holds true for at one instant is not necessarily the same person it holds true for at any other instant. The actual theorem is :$\backslash exists\; x\backslash in\; P.\backslash \; (\backslash rightarrow\; \backslash forall\; y\backslash in\; P.\backslash \; D(y)).\; \backslash ,$ where D is an arbitrary predicate and P is an arbitrary set. It was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book ''What Is the Name of this Book?'' == Proofs == The proof begins by recognizing it is true that either everyone in the pub is drinking, or at least one person in the pub is not drinking. Consequently, there are two cases to consider:〔〔 # Suppose everyone is drinking. For any particular person, it cannot be wrong to say that ''if that particular person is drinking, then everyone in the pub is drinking'' — because everyone is drinking. Because everyone is drinking, then that one person must drink because when ' ''that person'' ' drinks ' ''everybody'' ' drinks, everybody includes that person.〔〔 # Otherwise at least one person is not drinking. For any nondrinking person, the statement ''if that particular person is drinking, then everyone in the pub is drinking'' is formally true: its antecedent ("that particular person is drinking") is false, therefore the statement is true due to the nature of material implication in formal logic, which states that "If P, then Q" is always true if P is false.〔〔 (These kinds of statements are said to be vacuously true.) A slightly more formal way of expressing the above is to say that, if everybody drinks, then anyone can be the witness for the validity of the theorem. And if someone does not drink, then that particular non-drinking individual can be the witness to the theorem's validity. The proof above is essentially model-theoretic (can be formalized as such). A purely syntactic proof is possible and can even be mechanized (in Otter for example), but only for an equisatisfiable rather than an equivalent negation of the theorem.〔Marc Bezem , Dimitri Hendriks (2008) (Clausification in Coq )〕 Namely, the negation of the theorem is : $\backslash neg\; \backslash ,$ By Skolemization the above is equisatisfiable with : $\backslash forall\; x\; .\backslash \; (\backslash wedge\; \backslash neg\; D(f(x)))\backslash ,$ The resolution of the two clauses $D(x)$ and $\backslash neg\; D(f(x))$ results in an empty set of clauses (i.e. a contradiction), thus proving the negation of the theorem is unsatisfiable. The resolution is slightly non-straightforward because it involves a search based on Herbrand's theorem for ground instances that are propositionally unsatisfiable. The bound variable ''x'' is first instantiated with a constant ''d'' (making use of the assumption that the domain is non-empty), resulting in the Herbrand universe:〔 : $\backslash$ One can sketch the following natural deduction:〔 $$ \cfrac \forall_E } \wedge_E \qquad \cfrac \forall_E } \wedge_E } \ \Rightarrow_E Or spelled out: # Instantiating ''x'' with ''d'' yields $(\backslash wedge\; \backslash neg\; D(f(d)))$ which implies $\backslash neg\; D(f(d))$ # ''x'' is then instantiated with ''f(d)'' yielding $(\backslash wedge\; \backslash neg\; D(f(f(d))))$ which implies $D(f(d))$. Observe that $\backslash neg\; D(f(d))$ and $D(f(d))$ unify syntactically in their predicate arguments. An (automated) search thus finishes in two steps: # $D(d)\; \backslash wedge\; \backslash neg\; D(f(d))$ # $D(d)\; \backslash wedge\; \backslash underline\; \backslash wedge\; \backslash neg\; D(f(f(d)))$ The proof by resolution given here uses the law of excluded middle, the axiom of choice, and non-emptiness of the domain as premises.〔 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Drinker paradox」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.